$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), $L_{1}$, $L_{2}$:$T$ List.
\\[0ex]no\_repeats($T$;$L_{1}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L_{2}$) $\Leftrightarrow$ ($x$ $\in$ $L_{1}$) \& $P$($x$)) \& ($\forall$$x$, $y$:$T$. $x$ before $y$ $\in$ $L_{2}$ $\Rightarrow$ $x$ before $y$ $\in$ $L_{1}$)
\\[0ex]$\Rightarrow$ filter($P$;$L_{1}$) $=$ $L_{2}$